PRISM
=====
Version: 4.5.dev
Date: Fri Feb 26 16:41:55 CET 2021
Hostname: christopher
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 ij.50.prism ij.50.props --property stable
Parsing model file "ij.50.prism"...
Type: MDP
Modules: process0 process1 process2 process3 process4 process5 process6 process7 process8 process9 process10 process11 process12 process13 process14 process15 process16 process17 process18 process19 process20 process21 process22 process23 process24 process25 process26 process27 process28 process29 process30 process31 process32 process33 process34 process35 process36 process37 process38 process39 process40 process41 process42 process43 process44 process45 process46 process47 process48 process49
Variables: q0 q1 q2 q3 q4 q5 q6 q7 q8 q9 q10 q11 q12 q13 q14 q15 q16 q17 q18 q19 q20 q21 q22 q23 q24 q25 q26 q27 q28 q29 q30 q31 q32 q33 q34 q35 q36 q37 q38 q39 q40 q41 q42 q43 q44 q45 q46 q47 q48 q49 num_tokens_var
Parsing properties file "ij.50.props"...
1 property:
(1) "stable": Pmax=? [ F ((q0+q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21+q22+q23+q24+q25+q26+q27+q28+q29+q30+q31+q32+q33+q34+q35+q36+q37+q38+q39+q40+q41+q42+q43+q44+q45+q46+q47+q48+q49)=1) ]
---------------------------------------------------------------------
Model checking: "stable": Pmax=? [ F ((q0+q1+q2+q3+q4+q5+q6+q7+q8+q9+q10+q11+q12+q13+q14+q15+q16+q17+q18+q19+q20+q21+q22+q23+q24+q25+q26+q27+q28+q29+q30+q31+q32+q33+q34+q35+q36+q37+q38+q39+q40+q41+q42+q43+q44+q45+q46+q47+q48+q49)=1) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 50 iterations in 0.03 seconds (average 0.000680, setup 0.00)
Time for model construction: 0.116 seconds.
Type: MDP
States: 1125899906842623 (1 initial)
Transitions: 49258120924364800
Choices: 28147497671065600
Transition matrix: 6073 nodes (3 terminal), 49258120924364800 minterms, vars: 56r/56c/49nd
Warning: Switching to MTBDD engine, as number of states is too large for Sparse engine.
Prob0A: 50 iterations in 2.61 seconds (average 0.052280, setup 0.00)
Prob1E: 51 iterations in 3.22 seconds (average 0.063196, setup 0.00)
yes = 1125899906842623, no = 0, maybe = 0
Value in the initial state: 1.0
Time for model checking: 5.891 seconds.
Result: 1.0 (value in the initial state)
Overall running time: 6.275 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.